$\forall$$R$:es\_realizer\{i:l\}. Rda($R$) $\in$ fpf(Knd; $k$.Type)